\section{Prueba de correctitud para Mini-AES}
Debemos probar que la implementación aquí presentada es correcta, es decir que cumple con su especificación, la cual fue vista en la introducción mediante la ecuación~\ref{theo:inverse}.
Para realizar la prueba tomamos un enfoque \textit{top-down} de manera que comenzamos planteándonos el teorema cuya demostración implica la correctitud de nuesta codificación de Mini-AES, que es el siguiente:
\begin{lstlisting}
Theorem hoare_miniaes : forall m00 m01 m10 m11,
          0 <= m00 < 16 ->
          0 <= m01 < 16 ->
          0 <= m10 < 16 ->
          0 <= m11 < 16 ->
          sbox_defined miniSbox ->
          sboxInverse_defined miniSboxInv ->
          multTable_defined multTable ->
     {{ fun st => exists (matr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val matr) /\
                  matrix_defined matr m00 m01 m10 m11 /\
                  preConditions st }}
     miniAES.encrypt mid miniSboxId multTableId kid0 kid1 kid2;
     miniAES.decrypt mid miniSboxInvId multTableId kid0 kid1 kid2
     {{ fun st =>  exists (newMatr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val newMatr) /\
                  matrix_defined newMatr m00 m01 m10 m11 /\
                  preConditions st }}.
\end{lstlisting}
Como se puede ver, se están defininendo cuatro parámetros de entrada que son \texttt{m00}, \texttt{m01}, \texttt{m10} y \texttt{m11} los cuales representan las cuatro posiciones en la matriz de estado y se impone como condición sobre ellos que su valor se encuentre entre los posibles valores que puede tomar un nibble, que al tener 4 bits estos pueden representar 16 valores entre 0 y 15. Luego pueden observarse las hipótesis que debemos requerir sobre la tabla de sustitución \texttt{miniSbox}, su inversa \texttt{miniSboxInv} y la tabla de multiplicación \texttt{multTable}, dichas definiciones simplemente definen el valor que debe retornar la matriz para cada posición que sea accedida.
Finalmente nuestro objetivo es probar que las funciones \texttt{encrypt} y \texttt{decrypt} son inversas y que por lo tanto si aplicamos primero una y luego la otra sobre la misma variable, al finalizar el resultado almacenado en dicha variable contiene los mismos valores iniciales. Para realizar dicho planteo utilizamos la lógica de Hoare. Definimos un estado inicial en el cual existe una matriz almacenada en la variable \texttt{mid}: \texttt{st mid = Some (byte\_matrix\_val matr)} y cuyos valores son los parámetros de entrada: \texttt{matrix\_defined matr m00 m01 m10 m11}; en \texttt{preConditions} resumimos las condiciones referentes a la clave y las tablas de sustitución y multiplicación que deberán mantenerse invariantes durante todos los pasos de la prueba, esto es, que tanto las claves como las tablas se encuentren almacenadas en sus correspondientes variables y que sus valores no sean modificados en ningún momento.
En las post condiciones se puede ver que demostraremos la existencia de una matriz de estado, almacenada en el mismo lugar que la matriz inicial y cuyos cuatro valores son exactamente iguales.
La estructura general de la prueba es la siguiente:
\begin{description}
  \item[Introducir variables] Durante la prueba vamos a necesitar la existencia de algunos valores, por ejemplo al acceder a una posición de la tabla \texttt{s-box} sabemos que si se accede a una posición correcta, la tabla retorna un nibble. Esto lo utilizaremos para instanciar existenciales a lo largo de la prueba.
  \item[Aplicar lógica de Hoare] Utilizando lemas intermedios que ya tenemos demostrados, vamos aplicando uno a uno los pasos del algoritmo siguiendo la lógica de Hoare, demostrando las pre condiciones de cada paso a partir de las post condiciones del paso anterior.
  \item[Verificar correctitud] Al llegar al final de la ejecución del algoritmo, tendremos que demostrar como objetivo final que la matriz que se encuentra en la variable \texttt{mid} efectivamente tiene los valores que queremos demostrar, esto es \texttt{matrix\_defined x m00 m01 m10 m11}. Para demostrarlo tenemos \texttt{matrix\_defined x (xor x20 k2\_00) (xor x21 k2\_01) (xor x22 k2\_10) (xor x23 k2\_11)} y suficientes reglas que nos permiten relacionar \texttt{x20}, \texttt{x21}, \texttt{x22} y \texttt{x23} con \texttt{m00}, \texttt{m01}, \texttt{m10} y \texttt{m11} a través de las transformaciones que fueron siendo aplicadas.
\end{description}
\subsection*{Introducir variables}
En esta primera etapa simplemente aplicamos la táctica \textbf{destruct} pasando como argumento el término \texttt{get\_some} aplicado sobre los nibbles que queremos obtener. Por ejemplo, el primer \textbf{destruct} de la prueba tiene la siguiente forma:
\begin{align*}
\texttt{destruct (get\_some 1 16 0 (xor m00 k2\_00) miniSbox) as [x0 H0].}
\end{align*}
Esto nos genera como hipótesis:
\begin{align*}
& \texttt{x0: Byte} \\
& \texttt{H0: get Byte 1 16 0 (xor m00 k2\_00) miniSbox = Some x0}
\end{align*}
Luego \texttt{x0} será utilizado al aplicar el lema \texttt{hoare\_nibble\_sub} en la etapa de utilizar la lógica de Hoare y \texttt{H0} será utilizado en la etapa de verificar correctitud para recuperar el valor de \texttt{m00}.

\subsection*{Aplicar lógica de Hoare}
En esta parte lo que haremos será ir desarmando el algoritmo, separándolo paso a paso, de forma de poder observar el estado y probar su consistencia al aplicar cada una de las operaciones. Para esto hacemos fuerte uso de la lógica de Hoare, utilizando la regla \texttt{hoare\_seq} podemos separar el algoritmo en cada sentencia lo cual nos obliga a probar que el estado final de una operación sirve como estado inicial para la siguiente, aplicado sucesivas veces hasta probar el estado final tal como lo tenemos definido en el teorema.
\input{PruebasTex/hoare_miniaes}
En la figura~\ref{tree:hoare_miniaes} podemos observar el árbol de la prueba, donde se separa el Mini-AES en operaciones hasta llegar a las transformaciones básicas del algoritmo en las hojas del árbol, para las cuales creamos lemas auxiliares. Cada uno de estos lemas debe tomar en su estado inicial al estado final del anterior, o por lo menos se debe poder probar uno a partir del otro, notar que al aplicar \texttt{hoare\_seq} generamos variables existenciales para los nuevos estados st$_i$, y al aplicar los lemas auxiliares, estamos determinando realmente sus predicados.
Los lemas auxiliares mencionados son:
\begin{enumerate}
\item \texttt{hoare\_key\_addition}
\item \texttt{hoare\_shiftrow}
\item \texttt{hoare\_nibble\_sub}
\item \texttt{hoare\_nibble\_sub\_inv}
\item \texttt{hoare\_mix\_columns}
\end{enumerate}
Estos lemas los escribimos de forma de poder aplicarlos directamente en la demostración de Mini-AES, por ejemplo en la primera aplicación de \texttt{nibble\_sub} aplicamos el lema de la siguiente forma:
\begin{align*}
\texttt{apply hoare\_nibble\_sub with (s00:=x0)(s01:=x1)(s10:=x2)(s11:=x3).}
\end{align*}
Precisaremos además de los lemas auxiliares que nos permiten separar cada una de las instrucciones y los que nos permiten relajar las pre o post condiciones y poder aplicar los lemas mencionados antes:
\begin{enumerate}[(a)]
\item \texttt{hoare\_seq}
\item \texttt{hoare\_consequence\_pre}
\item \texttt{hoare\_consequence\_post}
\end{enumerate}
\subsection{hoare\_key\_addition}
\begin{lstlisting}
Lemma hoare_key_addition : forall m00 m01 m10 m11 kid k00 k01 k10 k11 key,
               equal_id mid kid = false ->
     {{ fun st => exists (matr: Matrix Byte 2 2),
                  matrix_defined key k00 k01 k10 k11 /\
                  st mid = Some (byte_matrix_val matr) /\
                  matrix_defined matr m00 m01 m10 m11 /\
                  st kid = Some (byte_matrix_val key) /\
                  preConditions st }}
     miniAES.keyAddition mid kid
     {{ fun st => exists (newMatr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val newMatr) /\
                  matrix_defined newMatr (xor m00 k00) (xor m01 k01) (xor m10 k10) (xor m11 k11) /\
                  preConditions st }}.
\end{lstlisting}
Esta prueba la realizamos aplicando los lemas \texttt{hoare\_matrix\_xor\_ij} para cada posición $\{i,j\}$ de la matriz de estado ya que la operación \texttt{keyAddition} solamente realiza un \texttt{xor} por cada posición y su correspondiente en la clave.\\
\input{PruebasTex/hoare_keyAddition}
\subsection*{hoare\_xor\_ij}
Mostramos \texttt{hoare\_xor\_11}, las demostraciones para las demás posiciones son análogas.
\begin{lstlisting}
Theorem hoare_matrix_xor_11 : forall (mid kid:Id)(key: Matrix Byte 2 2)
				(m00 m01 m10 m11 k00 k01 k10 k11: Byte),
                    equal_id mid kid = false ->
                    equal_id mid miniSboxId = false ->  
                    equal_id mid miniSboxInvId = false ->
                    equal_id mid multTableId = false ->
                    equal_id mid kid0 = false ->  
                    equal_id mid kid1 = false ->
                    equal_id mid kid2 = false ->
    {{ fun st => exists (matr: Matrix Byte 2 2), 
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 st kid = Some (byte_matrix_val key) /\
                 matrix_defined key k00 k01 k10 k11 /\
                 preConditions st }}
      mid[1][1] ::= (mid[1][1] xor kid[1][1])
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr'  m00 m01 m10 (xor m11 k11) /\
                 st kid = Some (byte_matrix_val key) /\
                 matrix_defined key k00 k01 k10 k11 /\
                 preConditions st }}.
\end{lstlisting}
Para probar esto primero aplicamos el lema \texttt{hoare\_matrix\_set}\footnote{Explicar antes} lo cual nos sirve para probar que al modificar la posición de la matriz con el nuevo valor, se cumple la postcondición de nuestro lema. Pero ahora debemos probar que las precondiciones del lema se cumplen en un estado en el que sustituimos la matriz de estado por otra matriz que es justamente la matriz con el valor cambiado:
\begin{lstlisting}
exists matr' : Matrix Byte 2 2,
  Update st mid0 (byte_matrix_val matr2) mid0 = Some (byte_matrix_val matr') /\
  matrix_defined matr' m00 m01 m10 (xor m11 k11) /\
  Update st mid0 (byte_matrix_val matr2) kid = Some (byte_matrix_val key) /\
  matrix_defined key k00 k01 k10 k11 /\
  preConditions (Update st mid0 (byte_matrix_val matr2))
\end{lstlisting}
Luego de utilizar \texttt{inversion} para transformar algunas hipótesis, contamos con lo siguiente:
\begin{lstlisting}
(a) st mid0 = Some (byte_matrix_val matr1)
(b) st mid0 = Some (byte_matrix_val x)
(c) matrix_defined x m00 m01 m10 m11
(d) set Byte 2 2 matr1 1 1 (xor m11 k11) = Some matr2
\end{lstlisting}
De (a) y (b) podemos deducir que \texttt{x = matr1} y sustituir en (c), de forma que nos quedan:
\begin{lstlisting}
(c) matrix_defined matr1 m00 m01 m10 m11
(d) set Byte 2 2 matr1 1 1 (xor m11 k11) = Some matr2
\end{lstlisting}
Si ahora elegimos como testigo a \texttt{matr2}, Coq nos exige probar:
\begin{lstlisting}
Update st mid0 (byte_matrix_val matr2) mid0 = Some (byte_matrix_val matr2) /\
matrix_defined matr2 m00 m01 m10 (xor m11 k11) /\
Update st mid0 (byte_matrix_val matr2) kid = Some (byte_matrix_val key) /\
matrix_defined key k00 k01 k10 k11 /\
preConditions (Update st mid0 (byte_matrix_val matr2))
\end{lstlisting}
La primera ecuación se prueba trivialmente computando la función Update y para la segunda aplicamos directamente el lema \texttt{matrix\_get\_set\_11}\footnote{Explicar antes} para el cual nos basta con utilizar las hipótesis (c) y (d). El resto de ecuaciones se encuentran directamente en las hipótesis, solo debemos utilizar las precondiciones de que \texttt{mid} sea distinto a las demás variables.

\subsection{hoare\_shift\_row}
\begin{lstlisting}
Lemma hoare_shiftrow : forall mid m00 m01 m10 m11,
                equal_id miniAES.aux mid = false ->
                equal_id mid miniAES.aux = false -> 
                equal_id mid miniSboxId = false -> 
                equal_id mid miniSboxInvId = false ->
                equal_id mid multTableId = false ->
                equal_id mid kid0 = false ->  
                equal_id mid kid1 = false -> 
                equal_id mid kid2 = false ->
     {{ fun st => exists (matr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val matr) /\
                  matrix_defined matr m00 m01 m10 m11 /\
                  preConditions st }}
     miniAES.shiftRow mid
     {{ fun st => exists (newMatr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val newMatr) /\
                  matrix_defined newMatr m00 m01 m11 m10 /\
                  preConditions st }}.
\end{lstlisting}
Puede observase en el código de \texttt{shiftRow} que el mismo consta de tres asignaciones, sin embargo cada una de las asignaciones es un tipo de expresión distinta:
\begin{enumerate}
\item Asignación a una variable de tipo \texttt{Byte}, a partir del acceso a una matriz.
\item Modificación de la posición de una matriz, a partir del acceso a otra matriz.
\item Modificación de la posición de una matriz, a partir de una variable de tipo \texttt{Byte}.
\end{enumerate}
Para cada tipo de expresión generamos un lema que muestre la transformación realizada sobre el estado al evaluar la misma, luego para probar \texttt{hoare\_shift\_row} simplemente aplicamos dichos lemas en orden. Estos tres lemas son:
\begin{enumerate}
\item \texttt{hoare\_byte\_matrix\_asgn\_10}
\item \texttt{hoare\_matrix\_matr\_10\_11}
\item \texttt{hoare\_matrix\_id\_11}
\end{enumerate}
\input{PruebasTex/hoare_shift_row}

\subsubsection{hoare\_byte\_matrix\_asgn}
\begin{lstlisting}
Lemma hoare_byte_matrix_asgn_10 : forall (mid X: Id) m00 m01 m10 m11, 
                equal_id X mid = false -> 
                equal_id X miniSboxId = false -> 
                equal_id X miniSboxInvId = false ->
                equal_id X multTableId = false ->
                equal_id X kid0 = false ->  
                equal_id X kid1 = false -> 
                equal_id X kid2 = false ->
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               preConditions st }}
      byte X ::= (byte_exp_matrix mid 1 0)
  {{ fun st => exists (matr: Matrix Byte 2 2),
               st X = Some (byte_val m10) /\
               st mid = Some (byte_matrix_val matr) /\
               matrix_defined matr m00 m01 m10 m11 /\
               preConditions st}}.
\end{lstlisting}
Esta prueba la comenzamos aplicando \texttt{hoare\_asgn}\footnote{Explicar antes}, que nos permite probar que se cumplen las postcondiciones al evaluar la instrucción. Para terminar debemos probar que se cumplen las precondiciones del lema en un nuevo estado en el que sustituimos la variable \texttt{X} por la posición accedida en la matriz, esto es:
\begin{lstlisting}
exists matr : Matrix Byte 2 2,
  Update st X (byte_val bb) X = Some (byte_val m10) /\
  Update st X (byte_val bb) mid0 = Some (byte_matrix_val matr) /\
  matrix_defined matr m00 m01 m10 m11 /\
  preConditions (Update st X (byte_val bb))
\end{lstlisting}
Para ello aplicamos \texttt{inversion} para transformar las hipótesis y contamos con las siguientes:
\begin{enumerate}[(a)]
\item \texttt{matrix\_defined matr' m00 m01 m10 m11}
\item \texttt{get Byte 2 2 1 0 matr' = Some bb}
\item \texttt{st mid0 = Some (byte\_matrix\_val matr')}
\end{enumerate}
Entonces podemos utilizar \texttt{matr'} como testigo. De (a) y (b) podemos deducir:
\begin{align*}
\texttt{Some m10 = get Byte 2 2 1 0 matr' = Some bb} \rightarrow \texttt{Some m10 = Some bb} \rightarrow \texttt{m10 = bb}
\end{align*}
Y con esto la primera condición separada por \texttt{and}s se cumple trivialmente. Luego contando con que \texttt{X} es distinto de \texttt{mid0}, la segunda condición se convierte directamente en nuestra hipótesis (c). La tercera condición es exactamente nuestra hipótesis (a) y la cuarta se encuentra en las hipótesis si descartamos que \texttt{X} sea igual a alguna de las variables utilizadas en \texttt{preConditions}, lo también se encuentra en las hipótesis del lema.

\subsubsection{hoare\_matrix\_matr}
\begin{lstlisting}
Lemma hoare_matrix_matr_10_11 : forall (mid bid:Id)(bval:Byte) m00 m01 m10 m11,
               equal_id mid bid = false -> 
               equal_id mid miniSboxId = false -> 
               equal_id mid miniSboxInvId = false ->
               equal_id mid multTableId = false ->
               equal_id mid kid0 = false ->  
               equal_id mid kid1 = false -> 
               equal_id mid kid2 = false ->
    {{ fun st => exists (matr: Matrix Byte 2 2),
                 st bid = Some (byte_val bval) /\
                 st mid = Some (byte_matrix_val matr) /\
                 matrix_defined matr m00 m01 m10 m11 /\
                 preConditions st }}
      instr_matrix_set mid 1 0 (byte_exp_matrix mid 1 1)
    {{ fun st => exists (matr': Matrix Byte 2 2),
                 st bid = Some (byte_val bval) /\
                 st mid = Some (byte_matrix_val matr') /\
                 matrix_defined matr' m00 m01 m11 m11 /\
                 preConditions st }}.
\end{lstlisting}
Para comenzar la prueba aplicamos \texttt{hoare\_matrix\_set}\footnote{Explicar antes}, esto nos permite demostrar que al ejecutar la asignación en la posición ${1,0}$ de la matriz se cumplen las postcondiciones del lema. Sin embargo, dicho lema nos impone condiciones que se deben cumplir para poder aplicarlo, entonces debemos probar que dichas condiciones se cumplen a partir de las precondiciones de nuestro lema objetivo.
Luego de aplicar \texttt{hoare\_matrix\_set} debemos probar lo siguiente:
\begin{lstlisting}
exists matr : Matrix Byte 2 2,
  Update st mid0 (byte_matrix_val m1) bid = Some (byte_val bval) /\
  Update st mid0 (byte_matrix_val m1) mid0 = Some (byte_matrix_val matr') /\
  matrix_defined matr' m00 m01 m11 m11 /\
  preConditions (Update st mid0 (byte_matrix_val m1))
\end{lstlisting}
En este momento tenemos hipótesis suficientes como para encontrar el testigo, alcanza con saber:
\begin{lstlisting}
matrix_defined x m00 m01 m10 m11
\end{lstlisting}
Aplicamos el lema \texttt{set\_matrix} de la siguiente forma:
\begin{lstlisting}
elim (set_matrix x 1 0 2 2 x b)
\end{lstlisting}
Y ahora sabemos como hipótesis lo siguiente:
\begin{lstlisting}
set Byte 2 2 x 1 0 b = Some x0
\end{lstlisting}
\texttt{x0} es nuestro testigo, ya que sabemos que tiene los mismos valores que \texttt{x}, a excepción de la posición ${1,0}$ donde asignamos el valor \texttt{b} que, como veremos más adelate es igual a \texttt{m11}.
Elegimos entonces nuestro testigo:
\begin{lstlisting}
exists x0
\end{lstlisting}
Por lo cual debemos probar:
\begin{lstlisting}
Update st mid0 (byte_matrix_val m1) bid = Some (byte_val bval) /\
Update st mid0 (byte_matrix_val m1) mid0 = Some (byte_matrix_val x0) /\
matrix_defined x0 m00 m01 m11 m11 /\
preConditions (Update st mid0 (byte_matrix_val m1))
\end{lstlisting}
Utilizando \texttt{split} separamos cada uno de los predicados. El primero es trivial, sabemos que \texttt{mid0} es distinto de \texttt{bid} y por lo tanto solo debemos probar \texttt{st bid = Some (byte\_val bval)} lo cual tenemos como hipótesis.
Para el segundo, debemos probar básicamente \texttt{m1 = x0} y para ello basta con notar las siguientes dos hipótesis:
\begin{lstlisting}
set Byte 2 2 x 1 0 b = Some x0
set Byte 2 2 x 1 0 b = Some m1
\end{lstlisting}
Es suficiente con sustituir \texttt{set Byte 2 2 x 1 0 b} de una ecuación en la otra y la igualdad se demuestra sencillamente.\\
El tercer predicado nos exige \texttt{matrix\_defined x0 m00 m01 m11 m11}. Contamos con las siguientes hipótesis:
\begin{lstlisting}
(a) matrix_defined x m00 m01 m10 m11
(b) get Byte 2 2 1 1 x = Some b
(c) set Byte 2 2 x 1 0 b = Some x0
\end{lstlisting}
De (a) y (b) podemos inferir la igualdad entre \texttt{m11} y \texttt{b} que anteriormente mencionamos, ya que (a) implica que \texttt{get Byte 2 2 1 1 x = Some m11}. Luego sustituyendo \texttt{b} por \texttt{m11} en (c) tenemos \texttt{set Byte 2 2 x 1 0 m11 = Some x0}. Recordemos que nuestro objetivo para este tercer predicado es:
\begin{lstlisting}
matrix_defined x0 m00 m01 m11 m11
\end{lstlisting}
Si en este momento aplicamos el lema \texttt{matrix\_get\_set\_10}\footnote{Explicar}, de la siguiente forma:
\begin{lstlisting}
apply matrix_get_set_10 with (matr:=x)(m10:=m10).
\end{lstlisting}
Entonces Coq nos va a exigir probar:
\begin{lstlisting}
matrix_defined x m00 m01 m10 m11
set Byte 2 2 x 1 0 m11 = Some x0
\end{lstlisting}
Ambos predicados existen exactamente en nuestras hipótesis. \\
Finalmente el predicado sobre \texttt{preConditions} se resuelve de la misma forma que en el resto de los lemas ya que esos valores so constantes y no fueron modificados en ningún momento.

\subsubsection{hoare\_matrix\_id\_11}

\subsection{hoare\_nibble\_sub}
\begin{lstlisting}
Lemma hoare_nibble_sub : forall m00 m01 m10 m11 s00 s01 s10 s11,
           get Byte 1 16 0 m00 miniSbox = Some s00 ->
           get Byte 1 16 0 m01 miniSbox = Some s01 ->
           get Byte 1 16 0 m10 miniSbox = Some s10 ->
           get Byte 1 16 0 m11 miniSbox = Some s11 ->
     {{ fun st => exists (matr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val matr) /\
                  matrix_defined matr m00 m01 m10 m11 /\
                  preConditions st}}
     miniAES.nibbleSub mid miniSboxId
     {{ fun st => exists (newMatr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val newMatr) /\
                  matrix_defined newMatr s00 s01 s10 s11 /\
                  preConditions st }}.
\end{lstlisting}
\subsection{hoare\_nibble\_sub\_inv}
\begin{lstlisting}
Lemma hoare_nibble_sub_inv : forall m00 m01 m10 m11 s00 s01 s10 s11,
           get Byte 1 16 0 m00 miniSboxInv = Some s00 ->
           get Byte 1 16 0 m01 miniSboxInv = Some s01 ->
           get Byte 1 16 0 m10 miniSboxInv = Some s10 ->
           get Byte 1 16 0 m11 miniSboxInv = Some s11 ->
     {{ fun st => exists (matr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val matr) /\
                  matrix_defined matr m00 m01 m10 m11 /\
                  preConditions st}}
     miniAES.nibbleSub mid miniSboxInvId
     {{ fun st => exists (newMatr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val newMatr) /\
                  matrix_defined newMatr s00 s01 s10 s11 /\
                  preConditions st }}.
\end{lstlisting}
\subsection{hoare\_mix\_columns}
\begin{lstlisting}
Lemma hoare_mix_columns : forall m00 m01 m10 m11 s00 s01 s10 s11,
           get Byte 16 16 m00 m10 multTable = Some s00 ->
           get Byte 16 16 m01 m11 multTable = Some s01 ->
           get Byte 16 16 m10 m00 multTable = Some s10 ->
           get Byte 16 16 m11 m01 multTable = Some s11 ->
     {{ fun st => exists (matr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val matr) /\
                  matrix_defined matr m00 m01 m10 m11 /\
                  preConditions st}}
     miniAES.mixColumn mid multTableId
     {{ fun st => exists (newMatr: Matrix Byte 2 2),
                  st mid = Some (byte_matrix_val newMatr) /\
                  matrix_defined newMatr s00 s01 s10 s11 /\
                  preConditions st }}.
\end{lstlisting}

\textcolor{red}{COMPLETAR}
